Fix effect substitutions, free names and unification of entities #1203
Conversation
| // Useful when substitutions have a transitive pattern [ a |-> b, b |-> c ] | ||
| return applySubstitution(subs, r) |
There was a problem hiding this comment.
Just to make sure: substitutions can never be cyclic?
Also, if not: do we really need to compute a fixed point here, or can we sort the substitutions topologically and apply them all at once?
There was a problem hiding this comment.
Just to make sure: substitutions can never be cyclic?
Nope, we check for cycles when generating substitution bindings.
Do we really need to compute a fixed point here, or can we sort the substitutions topologically and apply them all at once?
We could sort and apply all. Actually, I'm about 80% sure that we can assume that substitutions are already sorted topologically (because of the way they are constructed). However, I don't see a clear benefit of doing that over this? We are not iterating over all substitutions every time, we only call find - which sure, would be better in a simple array iteration, but then we have to worry about toposort.
There was a problem hiding this comment.
However, I don't see a clear benefit of doing that over this?
idk, I'm always for avoiding recursion if things can be achieved in a single call.
I guess here the overhead does not matter much, because the arrays are small, but even so, small delays add up and I'd avoid them, especially for compile-time checks.
There was a problem hiding this comment.
Makes sense. I'll keep this for now and improve it a performance-focused pass in the future. There are way more pressing performance problems and, then, I'll find a way to be very careful to not make regressions with the optmizations.
Hello
I finally figured out this substitution composition stuff! This should stabilize the effect checker a lot. Closes #1091 as a side effect. The main motivation for the fixes were problems encountered by @p-offtermatt (example in tests).
Turns out that substitution composition is really simple, and I was complicating it for the wrong reasons. As long as substitutions are properly applied to things before running unification on them, we can go back to the simple composition that we had at first, which is the normal thing from the papers.
This PR additions:
[v0, v1, v2]and[v1, v2], instead of throwing an error because we don't do unification of sets, we simplify them to[v0]and[]which easily results inv0 |->.applySubstitutionis now called in two new places on inferring effects for applications, ensuring the effects being unified are both updated with the latest substitutions. This makes it so the substitutions resulting from unification can compose with the existing ones with the classic composition algorithm, and therefore I removed the extra complexity I had added to ourcompose(and toapplySubstitutionsToSubstitutions).applySubstitutionwas fixed, as it was not working properly for substitutions like[a |-> b, b |-> c].From this list, (3), (4) and (5) should also be applicable for types. I'll do that as a followup and check if it solves any of our open issues for the type system.
CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality